loc:Id, T:Type, x:Id, L:Knd List. @loc only events in L change x:T  Realizer 

latex

Definitions	x:A. B(x), t  T, Realizer, @loc only events in L change x:T, Prop, x. t(x), x(s)
Lemmas	IdLnk wf, Id wf, fpf wf, Knd wf, decl-state wf, decl-type wf, unit wf